(set-info :source |fuzzsmt|)
(set-info :smt-lib-version 2.0)
(set-info :category "random")
(set-info :status unknown)
(set-logic QF_NRA)
(declare-fun v0 () Real)
(declare-fun v1 () Real)
(declare-fun v2 () Real)
(assert (let ((e3 3))
(let ((e4 6))
(let ((e5 (- v1 v0)))
(let ((e6 (* v1 e3)))
(let ((e7 (/ e3 (- e3))))
(let ((e8 (* (- e3) e6)))
(let ((e9 (+ v1 e7)))
(let ((e10 (- e6)))
(let ((e11 (* e5 v0)))
(let ((e12 (- v1 v0)))
(let ((e13 (+ e11 e9)))
(let ((e14 (- e13 e5)))
(let ((e15 (- e14)))
(let ((e16 (* e15 e15)))
(let ((e17 (/ e3 (- e3))))
(let ((e18 (- e7)))
(let ((e19 (+ v0 e7)))
(let ((e20 (* e5 (- e4))))
(let ((e21 (- e10)))
(let ((e22 (- e10 e17)))
(let ((e23 (- e13 e6)))
(let ((e24 (/ e4 (- e4))))
(let ((e25 (- e5 e20)))
(let ((e26 (* e11 (- e4))))
(let ((e27 (- v0)))
(let ((e28 (* e8 e25)))
(let ((e29 (+ e14 e6)))
(let ((e30 (- v0)))
(let ((e31 (+ e25 v1)))
(let ((e32 (+ e29 e15)))
(let ((e33 (+ v0 e6)))
(let ((e34 (/ e3 (- e4))))
(let ((e35 (/ e3 (- e3))))
(let ((e36 (+ e23 e22)))
(let ((e37 (- e15 e10)))
(let ((e38 (* e4 e17)))
(let ((e39 (- e12)))
(let ((e40 (/ e3 e4)))
(let ((e41 (+ e9 e35)))
(let ((e42 (+ e32 e32)))
(let ((e43 (* (- e3) e21)))
(let ((e44 (+ e36 e20)))
(let ((e45 (+ e7 v2)))
(let ((e46 (<= e35 e34)))
(let ((e47 (> e37 e43)))
(let ((e48 (= e37 e11)))
(let ((e49 (<= e22 e24)))
(let ((e50 (< e38 v0)))
(let ((e51 (<= e21 e8)))
(let ((e52 (> e15 e22)))
(let ((e53 (>= e44 e13)))
(let ((e54 (> e41 e23)))
(let ((e55 (>= e6 e20)))
(let ((e56 (>= e18 e25)))
(let ((e57 (< e21 e27)))
(let ((e58 (= v0 e28)))
(let ((e59 (>= e23 e35)))
(let ((e60 (distinct e25 e12)))
(let ((e61 (<= e25 e16)))
(let ((e62 (= e14 e22)))
(let ((e63 (<= v2 v2)))
(let ((e64 (< e10 v2)))
(let ((e65 (>= e31 e13)))
(let ((e66 (< v0 v1)))
(let ((e67 (= e41 e26)))
(let ((e68 (<= e9 e20)))
(let ((e69 (< e45 e23)))
(let ((e70 (= e37 e28)))
(let ((e71 (distinct e7 e32)))
(let ((e72 (distinct e5 e45)))
(let ((e73 (distinct e20 e17)))
(let ((e74 (< e11 e7)))
(let ((e75 (distinct e38 v2)))
(let ((e76 (> e30 e6)))
(let ((e77 (<= e11 e30)))
(let ((e78 (>= e19 e26)))
(let ((e79 (> e14 e17)))
(let ((e80 (= e34 e40)))
(let ((e81 (<= e12 e18)))
(let ((e82 (>= e38 e30)))
(let ((e83 (= e7 e6)))
(let ((e84 (<= e40 e33)))
(let ((e85 (> e33 e28)))
(let ((e86 (< e18 e25)))
(let ((e87 (> v2 e42)))
(let ((e88 (< e34 e16)))
(let ((e89 (distinct e42 e39)))
(let ((e90 (= e42 e5)))
(let ((e91 (<= e13 e21)))
(let ((e92 (= e35 e14)))
(let ((e93 (>= e11 e35)))
(let ((e94 (<= e23 e31)))
(let ((e95 (>= e9 e25)))
(let ((e96 (> v1 e8)))
(let ((e97 (= e9 e36)))
(let ((e98 (> e23 e33)))
(let ((e99 (< e14 e16)))
(let ((e100 (> e40 e6)))
(let ((e101 (>= v0 e6)))
(let ((e102 (distinct e18 e31)))
(let ((e103 (< e31 e43)))
(let ((e104 (<= e25 e31)))
(let ((e105 (< e18 e36)))
(let ((e106 (> e39 e15)))
(let ((e107 (> e28 e15)))
(let ((e108 (>= e21 e22)))
(let ((e109 (> e43 e42)))
(let ((e110 (= e8 e33)))
(let ((e111 (<= e6 e36)))
(let ((e112 (< e45 e29)))
(let ((e113 (< e25 e37)))
(let ((e114 (>= e11 e35)))
(let ((e115 (> e7 e14)))
(let ((e116 (>= e31 e33)))
(let ((e117 (= e34 e38)))
(let ((e118 (<= e25 e42)))
(let ((e119 (> e29 e25)))
(let ((e120 (> e9 e16)))
(let ((e121 (= e40 e32)))
(let ((e122 (distinct e33 v0)))
(let ((e123 (>= v1 e20)))
(let ((e124 (= e10 v1)))
(let ((e125 (> e36 e11)))
(let ((e126 (< e27 e25)))
(let ((e127 (<= e24 e18)))
(let ((e128 (= e9 e11)))
(let ((e129 (> e12 e23)))
(let ((e130 (distinct e41 e22)))
(let ((e131 (< e11 e34)))
(let ((e132 (> e7 e35)))
(let ((e133 (= e22 e10)))
(let ((e134 (= e23 e18)))
(let ((e135 (distinct e21 e28)))
(let ((e136 (> e9 e43)))
(let ((e137 (distinct e11 e41)))
(let ((e138 (<= e7 e11)))
(let ((e139 (> e9 e18)))
(let ((e140 (>= e39 e12)))
(let ((e141 (<= e15 e13)))
(let ((e142 (distinct e41 v0)))
(let ((e143 (> e35 e25)))
(let ((e144 (<= e20 e45)))
(let ((e145 (= e7 e30)))
(let ((e146 (<= e23 v1)))
(let ((e147 (< e20 e37)))
(let ((e148 (< e21 e38)))
(let ((e149 (>= e38 e15)))
(let ((e150 (> e31 e19)))
(let ((e151 (= e34 e12)))
(let ((e152 (distinct e42 e31)))
(let ((e153 (<= e19 e28)))
(let ((e154 (<= e34 e13)))
(let ((e155 (= e14 e38)))
(let ((e156 (= e7 e33)))
(let ((e157 (distinct e19 e41)))
(let ((e158 (= e28 e18)))
(let ((e159 (< e41 e10)))
(let ((e160 (>= v1 e37)))
(let ((e161 (distinct e30 e20)))
(let ((e162 (>= e38 e9)))
(let ((e163 (>= e36 e29)))
(let ((e164 (< e10 e14)))
(let ((e165 (> e34 e10)))
(let ((e166 (> e21 e43)))
(let ((e167 (> e43 e24)))
(let ((e168 (< e22 e13)))
(let ((e169 (> e15 e32)))
(let ((e170 (<= e40 e24)))
(let ((e171 (> e29 e38)))
(let ((e172 (<= e21 e44)))
(let ((e173 (<= e16 e37)))
(let ((e174 (<= v0 e27)))
(let ((e175 (< v2 e12)))
(let ((e176 (< e29 e29)))
(let ((e177 (< e32 e28)))
(let ((e178 (< e30 e43)))
(let ((e179 (> e16 e7)))
(let ((e180 (> e17 v1)))
(let ((e181 (< e42 v0)))
(let ((e182 (= e21 e23)))
(let ((e183 (> e34 e44)))
(let ((e184 (>= e32 e31)))
(let ((e185 (<= e23 e9)))
(let ((e186 (<= e10 e40)))
(let ((e187 (< e37 e34)))
(let ((e188 (> e37 v0)))
(let ((e189 (> e37 e29)))
(let ((e190 (= e44 v0)))
(let ((e191 (<= e37 e6)))
(let ((e192 (< e18 e27)))
(let ((e193 (distinct e32 e29)))
(let ((e194 (distinct e16 e37)))
(let ((e195 (distinct e9 e25)))
(let ((e196 (distinct e38 e41)))
(let ((e197 (<= e8 e32)))
(let ((e198 (distinct e25 v0)))
(let ((e199 (>= v2 e31)))
(let ((e200 (< e5 e42)))
(let ((e201 (= v0 v0)))
(let ((e202 (>= e22 e27)))
(let ((e203 (< e8 e5)))
(let ((e204 (< v0 e37)))
(let ((e205 (>= e38 e16)))
(let ((e206 (> e28 e32)))
(let ((e207 (> e13 e12)))
(let ((e208 (<= e42 e26)))
(let ((e209 (xor e123 e177)))
(let ((e210 (or e140 e63)))
(let ((e211 (ite e187 e95 e103)))
(let ((e212 (and e169 e147)))
(let ((e213 (ite e183 e81 e212)))
(let ((e214 (xor e180 e148)))
(let ((e215 (or e72 e80)))
(let ((e216 (ite e188 e143 e149)))
(let ((e217 (xor e56 e136)))
(let ((e218 (ite e65 e134 e191)))
(let ((e219 (or e210 e61)))
(let ((e220 (ite e94 e70 e146)))
(let ((e221 (or e98 e203)))
(let ((e222 (ite e133 e85 e64)))
(let ((e223 (not e173)))
(let ((e224 (=> e218 e126)))
(let ((e225 (xor e224 e219)))
(let ((e226 (or e117 e155)))
(let ((e227 (= e107 e138)))
(let ((e228 (= e179 e181)))
(let ((e229 (xor e152 e114)))
(let ((e230 (or e229 e121)))
(let ((e231 (xor e101 e161)))
(let ((e232 (ite e226 e225 e116)))
(let ((e233 (ite e60 e125 e127)))
(let ((e234 (not e55)))
(let ((e235 (or e164 e137)))
(let ((e236 (ite e182 e59 e171)))
(let ((e237 (and e78 e100)))
(let ((e238 (ite e209 e198 e207)))
(let ((e239 (= e208 e223)))
(let ((e240 (xor e184 e232)))
(let ((e241 (or e154 e106)))
(let ((e242 (ite e195 e69 e153)))
(let ((e243 (or e53 e178)))
(let ((e244 (= e189 e186)))
(let ((e245 (ite e131 e239 e119)))
(let ((e246 (= e145 e242)))
(let ((e247 (ite e112 e144 e246)))
(let ((e248 (not e96)))
(let ((e249 (not e62)))
(let ((e250 (ite e71 e194 e84)))
(let ((e251 (or e142 e141)))
(let ((e252 (not e174)))
(let ((e253 (xor e244 e170)))
(let ((e254 (=> e110 e204)))
(let ((e255 (or e67 e217)))
(let ((e256 (and e222 e92)))
(let ((e257 (and e193 e175)))
(let ((e258 (and e197 e118)))
(let ((e259 (xor e158 e47)))
(let ((e260 (not e243)))
(let ((e261 (or e176 e258)))
(let ((e262 (xor e250 e206)))
(let ((e263 (and e124 e91)))
(let ((e264 (and e245 e108)))
(let ((e265 (=> e54 e257)))
(let ((e266 (not e111)))
(let ((e267 (and e104 e185)))
(let ((e268 (xor e196 e115)))
(let ((e269 (not e83)))
(let ((e270 (xor e238 e260)))
(let ((e271 (not e255)))
(let ((e272 (xor e90 e256)))
(let ((e273 (xor e73 e99)))
(let ((e274 (ite e262 e199 e265)))
(let ((e275 (=> e166 e113)))
(let ((e276 (ite e151 e79 e268)))
(let ((e277 (not e88)))
(let ((e278 (=> e105 e159)))
(let ((e279 (or e48 e278)))
(let ((e280 (=> e201 e163)))
(let ((e281 (not e247)))
(let ((e282 (not e200)))
(let ((e283 (=> e75 e167)))
(let ((e284 (not e216)))
(let ((e285 (xor e214 e86)))
(let ((e286 (or e68 e77)))
(let ((e287 (xor e132 e284)))
(let ((e288 (and e270 e236)))
(let ((e289 (= e49 e52)))
(let ((e290 (=> e267 e122)))
(let ((e291 (= e264 e76)))
(let ((e292 (= e51 e150)))
(let ((e293 (or e286 e87)))
(let ((e294 (and e288 e266)))
(let ((e295 (xor e234 e172)))
(let ((e296 (= e276 e274)))
(let ((e297 (xor e279 e213)))
(let ((e298 (and e254 e261)))
(let ((e299 (=> e293 e248)))
(let ((e300 (=> e291 e277)))
(let ((e301 (= e269 e292)))
(let ((e302 (or e58 e253)))
(let ((e303 (ite e249 e298 e50)))
(let ((e304 (and e139 e241)))
(let ((e305 (xor e282 e66)))
(let ((e306 (=> e252 e192)))
(let ((e307 (=> e303 e46)))
(let ((e308 (= e227 e271)))
(let ((e309 (xor e97 e82)))
(let ((e310 (not e275)))
(let ((e311 (=> e130 e300)))
(let ((e312 (or e283 e290)))
(let ((e313 (and e251 e263)))
(let ((e314 (xor e165 e295)))
(let ((e315 (xor e233 e311)))
(let ((e316 (= e312 e57)))
(let ((e317 (and e305 e93)))
(let ((e318 (=> e109 e231)))
(let ((e319 (= e285 e228)))
(let ((e320 (=> e297 e309)))
(let ((e321 (= e315 e235)))
(let ((e322 (=> e310 e89)))
(let ((e323 (xor e319 e120)))
(let ((e324 (ite e230 e320 e280)))
(let ((e325 (not e272)))
(let ((e326 (= e304 e321)))
(let ((e327 (xor e221 e324)))
(let ((e328 (not e296)))
(let ((e329 (= e314 e190)))
(let ((e330 (or e205 e294)))
(let ((e331 (= e316 e327)))
(let ((e332 (not e237)))
(let ((e333 (xor e325 e317)))
(let ((e334 (= e128 e330)))
(let ((e335 (ite e202 e129 e74)))
(let ((e336 (ite e318 e162 e322)))
(let ((e337 (= e289 e307)))
(let ((e338 (or e156 e220)))
(let ((e339 (or e336 e215)))
(let ((e340 (or e329 e160)))
(let ((e341 (not e308)))
(let ((e342 (not e339)))
(let ((e343 (=> e340 e342)))
(let ((e344 (ite e168 e326 e302)))
(let ((e345 (not e335)))
(let ((e346 (ite e273 e287 e281)))
(let ((e347 (or e333 e102)))
(let ((e348 (=> e299 e334)))
(let ((e349 (xor e301 e345)))
(let ((e350 (=> e306 e135)))
(let ((e351 (=> e347 e157)))
(let ((e352 (xor e337 e331)))
(let ((e353 (or e313 e211)))
(let ((e354 (and e350 e259)))
(let ((e355 (xor e348 e348)))
(let ((e356 (and e353 e349)))
(let ((e357 (not e352)))
(let ((e358 (xor e351 e355)))
(let ((e359 (and e358 e358)))
(let ((e360 (or e328 e338)))
(let ((e361 (xor e357 e341)))
(let ((e362 (xor e344 e332)))
(let ((e363 (xor e359 e360)))
(let ((e364 (and e343 e363)))
(let ((e365 (or e354 e240)))
(let ((e366 (=> e361 e356)))
(let ((e367 (and e365 e366)))
(let ((e368 (xor e346 e362)))
(let ((e369 (= e323 e323)))
(let ((e370 (ite e369 e369 e369)))
(let ((e371 (= e368 e370)))
(let ((e372 (=> e367 e364)))
(let ((e373 (and e371 e372)))
e373
))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))

(check-sat)
